\begin{tabbing}
rng\{i:l\}
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\{\=$r$:rng\_sig\{i:l\}$\mid$ \+
\\[0ex]ring\_p(rng\_car($r$); rng\_plus($r$); rng\_zero($r$); rng\_minus($r$); rng\_times($r$); rng\_one($r$))
\\[0ex]$\wedge$ eqfun\_p(rng\_car($r$); rng\_eq($r$))\} 
\-
\end{tabbing}